package srt.tool;

import srt.ast.AssertStmt;
import srt.ast.AssignStmt;

public class SMTLIBQueryBuilder {

	private ExprToSmtlibVisitor exprConverter;
	private CollectConstraintsVisitor constraints;
	private String queryString = "";

	public SMTLIBQueryBuilder(CollectConstraintsVisitor ccv) {
		this.constraints = ccv;
		this.exprConverter = new ExprToSmtlibVisitor();
	}

	public void buildQuery() {
		StringBuilder query = new StringBuilder();
		query.append("\n\n(set-logic QF_BV)\n"
				+ "(define-fun tobv32 ((p Bool)) (_ BitVec 32) (ite p (_ bv1 32) (_ bv0 32)))\n");
		query.append("(define-fun tobool ((b (_ BitVec 32))) (Bool) (not (= b (_ bv0 32) )))\n");
		// TODO: Define more functions above (for convenience), as needed.

		// TODO: Declare variables, add constraints, add properties to check
		// here.

		for (String var : constraints.variableNames) {
			String line = "(declare-fun " + var + " () (_ BitVec 32))\n";
			query.append(line);
		}
		
		query.append(prepareOutputVariables());
		
		// Add constraints
		for (AssignStmt e : constraints.transitionNodes) {
			String line = "(assert ( = "
					+ exprConverter.visit(e.getLhs()) + ""
					+ exprConverter.visit(e.getRhs()) + "))\n";
			query.append(line);
		}

		query.append(generateAssertions());
		
		query.append("(check-sat)\n");
		
		query.append(getOtputVariables());
		
		queryString = query.toString();
	}

	private String generateAssertions(){
		StringBuilder sb = new StringBuilder();

		sb.append("(assert( or");
		
		for (AssertStmt stm1 : this.constraints.propertyNodes) {
			sb.append("(not " + exprConverter.visit(stm1.getCondition())
					+ ")");
		}
		sb.append("))\n");
		
		return sb.toString();
	}
	
	private String prepareOutputVariables(){
		
		StringBuilder sb = new StringBuilder();
		
		for (int i = 0; i < this.constraints.propertyNodes.size() ; ++i ) {
			String line = "(declare-fun prop" + i + " () (Bool))\n";
			sb.append(line);
			String line1 = "(assert (= prop" + i + " (not " +
					exprConverter.visit(constraints.propertyNodes.get(i).getCondition()) +")))\n";
			sb.append(line1);
		}
		
		return sb.toString();
	}
	
	private String getOtputVariables(){
		StringBuilder sb = new StringBuilder();

		sb.append("(get-value (");
		
		for (int i = 0; i < this.constraints.propertyNodes.size() ; ++i ) {
			sb.append(" prop" + i);
		}
		sb.append("))\n");
		
		return sb.toString();
	}
	
	public String getQuery() {
		return queryString;
	}

}
